A:Type, P:((A List)Prop). strong_safety(A;x.P(x))  Prop 

latex

Definitions	t  T, Prop, x(s), P  Q, x:A. B(x), L1  L2, strong_safety(T;tr.P(tr))
Lemmas	sublist wf